Date: Tue, 14 Jan 1997 22:21:01 GMT
Server: Apache/1.1.1
Content-type: text/html
Content-length: 14733
Last-modified: Thu, 02 Jan 1997 07:29:24 GMT

<HTML>
<HEAD>

<TITLE>Logic Software from CSLI</TITLE>
</HEAD>
<BODY BGCOLOR="#708090" LINK="#bfdedb"  VLINK="#045658" ALINK="#aef7f0"> 

<center> 
<A NAME="Top"><!WA0><IMG SRC="http://csli-www.stanford.edu/hp/csli.GIF" ALT="CSLI Logo"></A><P>

<H1>Logic Software from CSLI</H1>
<H3>By Jon Barwise and John Etchemendy</H3>
</center> 

<TABLE BORDER=6 ALIGN=CENTER VALIGN=TOP CELLPADDING=20>

        <TR>
        <TD VALIGN=TOP >
The text/software packages described here -- <!WA1><A HREF="#Hyperproof"><STRONG>Hyperproof</STRONG></A>, <!WA2><A HREF="#LOFOL"><STRONG>The Language of First-order Logic</STRONG></A>, <!WA3><A HREF="#Tarski"><STRONG>Tarski's World</STRONG></A> and <!WA4><A HREF="#Turing"><STRONG>Turing's World</STRONG></A> -- are all published by the <!WA5><A HREF="http://csli-www.stanford.edu/csli/csli.html">Center for the Study of Language and Information</A> and distributed by Cambridge University Press.  Click here for <!WA6><A HREF="http://csli-www.stanford.edu/hp/Ordering-info.html">ordering information</A>.  If you already own any of these packages, click here for <!WA7><A HREF="http://csli-www.stanford.edu/hp/Version-info.html">up-to-date version information</A> and other information of interest to current users.  Click here if you have any <!WA8><A HREF="http://csli-www.stanford.edu/hp/Comment-form.html">comments, suggestions or questions</A>.<P>

If you would like to read a new paper by Barwise and Etchemendy
describing the reasons they developed this software and how it has
changed their view of logic, check out "<!WA9><A HREF="http://csli-www.stanford.edu/hp/CVandNR.pdf">Computers,
Visualization, and the Nature of Reasoning</A>."  You will need
Adobe's Acrobat Reader to read this file.
        </TD>
        </TR>
</TABLE>
<P>
<HR size=4> 
<P>
<A NAME="Hyperproof"><STRONG>Hyperproof</STRONG></A><P> 


<CENTER> 
<TABLE BORDER=6 ALIGN=CENTER VALIGN=TOP CELLPADDING=7>

        <TR>
        <TD VALIGN=TOP >
<!WA10><A HREF="http://csli-www.stanford.edu/hp/Hyperproof-Mac-100.GIF"><!WA11><IMG SRC="http://csli-www.stanford.edu/hp/Hyperproof-Mac-25.GIF" border=0 ALT="Hyperproof cover"></A>  
        </TD>
        </TR>
</TABLE>
</CENTER> 
<P>
 

<STRONG>Hyperproof</STRONG> is a system for learning the principles of analytical reasoning and proof construction, consisting of a text and a Macintosh software program.  Unlike traditional treatments of first-order logic, Hyperproof combines graphical and sentential information, presenting a set of logical rules for integrating these different forms of information.  This strategy allows students to focus on the information content of proofs rather than the syntactic structure of sentences.  It also reflects the heterogeneity of information encountered in everyday reasoning. <P>

Using <STRONG>Hyperproof</STRONG> the student learns to construct proofs of both consequence and non-consequence using an intuitive proof system that extends the standard set of sentential rules to incorporate information represented graphically.  Proofs of consistency and inconsistency are also covered as well as independence proofs.  The <STRONG>Hyperproof</STRONG> software checks the logical validity of each type of proof.<P>

<STRONG>Hyperproof</STRONG> is compatible with various natural-deduction-style proof systems, including the system used in the authors' <STRONG>The Language of First-order Logic.</STRONG>
<BLOCKQUOTE>"<STRONG>Hyperproof</STRONG> is wonderful!  With it you can construct and check proofs in an expanded version of the language of <STRONG>Tarski's World</STRONG>.  And there is more, much more, another whole dimension.  <STRONG>Hyperproof</STRONG> lets you use pictorially-presented information and pictorially-oriented deduction techniques, in combination with sentences and syntactic rules, to reason about its block worlds.  It is an extraordinarily impressive programming achievement.  <STRONG>Hyperproof</STRONG> will make learning first-order logic enormously more fun."  --Carl Ginet, Cornell University
</BLOCKQUOTE>

<STRONG>Hyperproof</STRONG> is designed to be used in a first course in logic.  Since it presupposes familiarity with the program <STRONG>Tarski's World</STRONG>, it should be used in tandem with either the textbook <STRONG>The Language of First-order Logic</STRONG> or the stand-alone version of <STRONG>Tarski's World</STRONG> (<STRONG>Tarski "Lite"</STRONG>).  <STRONG>Hyperproof</STRONG> is currently available only for the Macintosh.  A Microsoft Windows version is under development.<P>
<!WA12><A HREF="http://csli-www.stanford.edu/hp/Ordering-info.html#Hproof"><!WA13><IMG SRC="http://csli-www.stanford.edu/hp/order-button.GIF" border=0> Ordering information</A>     <!WA14><A HREF="http://csli-www.stanford.edu/hp/Hproof1.html"><!WA15><IMG SRC="http://csli-www.stanford.edu/hp/hproof-button.GIF" border=0> Show me Hyperproof</A><P>

[<!WA16><A HREF="#Top">Top</A> | <!WA17><A HREF="http://csli-www.stanford.edu/hp/HproofTOC.html">Hyperproof Table of Contents</A> | <!WA18><A HREF="http://csli-www.stanford.edu/hp/Version-info.html">Information for current users</A> | <!WA19><A HREF="http://csli-www.stanford.edu/hp/Hproof5.html">Acknowledgements</A>]  
<HR size=4><P>

<A NAME="LOFOL"><STRONG>The Language of First-order Logic</STRONG> (Mac or PC)</A><P>

<CENTER> 
<TABLE BORDER=6 ALIGN=CENTER VALIGN=TOP CELLPADDING=7>

        <TR>
        <TD VALIGN=TOP >

<!WA20><A HREF="http://csli-www.stanford.edu/hp/LOFOL-Mac-100.GIF"><!WA21><IMG SRC="http://csli-www.stanford.edu/hp/LOFOL-Mac-25.GIF" border=0 ALT="Mac cover"></A> 

        </TD>
        <TD VALIGN=TOP>

 <!WA22><A HREF="http://csli-www.stanford.edu/hp/LOFOL-IBM-100.GIF"><!WA23><IMG SRC="http://csli-www.stanford.edu/hp/LOFOL-IBM-25.GIF" border=0 ALT="Windows cover"></A>

        </TD>
        </TR>
</TABLE>
</CENTER> 
<P>

  


<STRONG>The Language of First-order Logic</STRONG> presents a new approach to teaching first-order logic.  Taking advantage of the accompanying program
<STRONG>Tarski's World</STRONG>, the text skillfully balances the semantic conception of logic with methods of proof.  The book contains eleven
chapters, in four parts.  Part I is about propositional logic and Part II
covers quantifier logic.  Part III contains chapters on set theory and
inductive definitions.  Part IV contains advanced topics in logic,
including topics of importance in applications of logic in computer
science.  <STRONG>The Language of First-order Logic</STRONG> contains hundreds of
problems and exercises.<P>

An instructor's manual and instructor's disk are available to
accompany this book.  The instructor's manual, written by Ruth Eberle,
provides a wealth of material to make grading exercises and teaching
from the text easier.  The instructor's disk allows you to grade most
of the <STRONG>Tarski's World</STRONG> problems automatically, directly off the
student's disks.  It is possible to grade both IBM PC and Macintosh
disks using the Macintosh version of the program. 

<BLOCKQUOTE>"[<STRONG>The Language of First-order Logic</STRONG>] is packed with interesting exercises and problems which make imaginative use of [<STRONG>Tarski's World</STRONG>].  This is an excellent package and we recommend it highly as the basis of either a complete first course in logic or as an initial part of such a course."  --Doug Goldson, Steve Reeves and Richard Bornat, University of London</BLOCKQUOTE>

<BLOCKQUOTE>"<STRONG>The Language of First-order Logic</STRONG> and <STRONG>Tarski's World</STRONG> redress one of the main shortcomings of traditional beginning-level logic texts which emphasize the formal aspects of logic and pay scant attention to semantics.  <STRONG>Tarski's World</STRONG> sets a high standard for those who follow."  --Kevin Compton, Journal of Symbolic Logic.</BLOCKQUOTE> 

<BLOCKQUOTE>"The emphasis throughout is on the user doing logic by working the many problems in the text.  Recommended unreservedly as a fascinating approach to a fascinating subject."  --R. J. Wernick, Choice</BLOCKQUOTE>

<STRONG>The Language of First-order Logic</STRONG> comes packaged with the program <STRONG>Tarski's World</STRONG>.  Since <STRONG>Hyperproof</STRONG> uses an extension of the natural-deduction-style proof system taught in <STRONG>The Language of First-order Logic</STRONG>, it can be used to accompany this text.  <STRONG>The Language of First-order Logic</STRONG> is available in versions for Macintosh and Microsoft Windows.  A version of the software for computers running NeXTstep is also available.  To receive it, purchase a copy of either the Macintosh or Windows version and follow the instructions contained in the book.<P>

<!WA24><A HREF="http://csli-www.stanford.edu/hp/Ordering-info.html#LOFOL"><!WA25><IMG SRC="http://csli-www.stanford.edu/hp/order-button.GIF" border=0> Ordering information</A>     <!WA26><A HREF="http://csli-www.stanford.edu/hp/Tarski1.html"><!WA27><IMG SRC="http://csli-www.stanford.edu/hp/tarski-button.GIF" border=0> Show me Tarski's World</A><P>
[<!WA28><A HREF="#Top">Top</A> | <!WA29><A HREF="http://csli-www.stanford.edu/hp/LOFOLTOC.html">LOFOL Table of Contents</A> | <!WA30><A HREF="http://csli-www.stanford.edu/hp/Version-info.html">Information for current users</A> | <!WA31><A HREF="http://csli-www.stanford.edu/hp/Tarski5.html">Acknowledgements</A>]  

<HR size=4><P>

<A NAME="Tarski"><STRONG>Tarski "Lite"</STRONG> (Mac or PC)</A><P>

<CENTER> 
<TABLE BORDER=6 ALIGN=CENTER VALIGN=TOP CELLPADDING=7>

        <TR>
        <TD VALIGN=TOP >

<!WA32><A HREF="http://csli-www.stanford.edu/hp/Tarski-Mac-100.GIF"><!WA33><IMG SRC="http://csli-www.stanford.edu/hp/Tarski-Mac-25.GIF" border=0 ALT="Mac cover"></A> 

        </TD>
        <TD VALIGN=TOP>

 <!WA34><A HREF="http://csli-www.stanford.edu/hp/Tarski-IBM-100.GIF"><!WA35><IMG SRC="http://csli-www.stanford.edu/hp/Tarski-IBM-25.GIF" border=0 ALT="Windows cover"></A>

        </TD>
        </TR>
</TABLE>
</CENTER> 
<P>

  

<STRONG>Tarski's World</STRONG> is an innovative and enjoyable way to introduce
your students to the language of first-order logic.  Using this
program students quickly master the meaning of the connectives and
quantifiers, and soon become fluent in the symbolic language at the
core of modern logic.  <STRONG>Tarski's World</STRONG> allows the students to build
three-dimensional worlds and to describe them in first-order logic.
They evaluate the sentences in the constructed worlds and if their
evaluation is incorrect, the program provides them with a game that
leads them to understand where they went wrong.  <P>

<STRONG>Tarski's World</STRONG> is available in two ways, either alone (called <STRONG>Tarski's World 4.0</STRONG> or <STRONG>Tarski "Lite"</STRONG>) or as part of the logic textbook/software package called <STRONG>The Language of First-order Logic</STRONG>.<P>
  
<STRONG>Tarski "Lite"</STRONG>, the stand-alone package, is intended as a supplement to any standard logic text or for use by anyone who wants to learn the language.  The disk and manual contain over a hundred exercises from very basic to highly sophisticated.    

<BLOCKQUOTE>"If you have had a small amount of experience with a Macintosh and enjoy logical matters, then you will almost certainly enjoy using (or just playing with) this software for the Mac."  --George Boolos, Journal of Symbolic Logic</BLOCKQUOTE>

<BLOCKQUOTE>"The authors are pioneers.  [<STRONG>Tarski's World</STRONG>] is the only program that I know for teaching first-order semantics, and it sets a high standard.  I warmly recommend it."  --Wilfrid Hodges, Queen Mary College</BLOCKQUOTE>

<STRONG>Tarski "Lite"</STRONG> is available for Macintosh or Microsoft Windows.  A version of the software for computers running NeXTstep is also available.  To receive it, purchase a copy of either the Macintosh or Windows version and follow the instructions contained in the book.<P>

<!WA36><A HREF="http://csli-www.stanford.edu/hp/Ordering-info.html#Tarski"><!WA37><IMG SRC="http://csli-www.stanford.edu/hp/order-button.GIF" border=0> Ordering information</A>     <!WA38><A HREF="http://csli-www.stanford.edu/hp/Tarski1.html"><!WA39><IMG SRC="http://csli-www.stanford.edu/hp/tarski-button.GIF" border=0> Show me Tarski's World</A><P>
[<!WA40><A HREF="#Top">Top</A> | <!WA41><A HREF="http://csli-www.stanford.edu/hp/TarskiTOC.html">Tarski "Lite" Table of Contents</A> | <!WA42><A HREF="http://csli-www.stanford.edu/hp/Version-info.html">Information for current users</A> | <!WA43><A HREF="http://csli-www.stanford.edu/hp/Tarski5.html">Acknowledgements</A>] 
<HR size=4><P>
<A NAME="Turing"><STRONG>Turing's World</STRONG></A><P>

<CENTER> 
<TABLE BORDER=6 ALIGN=CENTER VALIGN=TOP CELLPADDING=7>

        <TR>
        <TD VALIGN=TOP >
<!WA44><A HREF="http://csli-www.stanford.edu/hp/Turing-Mac-100.GIF"><!WA45><IMG SRC="http://csli-www.stanford.edu/hp/Turing-Mac-25.GIF" border=0 ALT="Turing's World cover"></A>  
        </TD>
        </TR>
</TABLE>
</CENTER> 
<P>



<STRONG>Turing's World</STRONG> is a self-contained introduction to Turing machines,
one of the fundamental notions of logic and computer science.  The
text and accompanying diskette allow the user to design, debug, and
run sophisticated Turing machines in a graphical environment on the
Macintosh.<P>

<STRONG>Turing's World</STRONG> introduces users to the key concepts in
computability theory through a sequence of over 100 exercises and
projects.  Within minutes, users learn to build simple Turing machines
using a convenient package of graphical functions.  Exercises then
progress through a significant portion of elementary computability
theory, covering such topics as the Halting problem, the Busy Beaver
function, recursive functions, and undecidability.<P>

 Version 3.0 is an extensive revision and enhancement of earlier
releases of the program, allowing the construction of one-way and
two-way finite state machines (finite automata), as well as
nondeterministic Turing and finite-state machines.  Special exercises
allow users to expore these alternative machines.

<BLOCKQUOTE>"<STRONG>Turing's World</STRONG> is a delight....I heartily recommend [it]."  --James Moor, Teaching Philosophy</BLOCKQUOTE>

<BLOCKQUOTE>"<STRONG>Turing's World</STRONG> quite literally revolutionizes the way the fundamental theoretical issues of computing can be taught."  
--Keith Devlin, The Guardian
</BLOCKQUOTE>
<BLOCKQUOTE>"There is not the slightest hint of jargon anywhere in [<STRONG>Turing's World</STRONG>].  The explanations are so direct that a beginner will understand them and an old hand will enjoy them."  
--Wilfrid Hodges, Queen Mary College
</BLOCKQUOTE>
<BLOCKQUOTE>"The program and manual are the best introduction to Turing machines the reviewer knows of, or can imagine."  
--George Boolos, Journal of Symbolic Logic
</BLOCKQUOTE>

<!WA46><A HREF="http://csli-www.stanford.edu/hp/Ordering-info.html#Turing"><!WA47><IMG SRC="http://csli-www.stanford.edu/hp/order-button.GIF" border=0> Ordering information</A>     <!WA48><A HREF="http://csli-www.stanford.edu/hp/Turing1.html"><!WA49><IMG SRC="http://csli-www.stanford.edu/hp/turing-button.GIF" border=0> Show me Turing's World</A><P>
[<!WA50><A HREF="#Top">Top</A> | <!WA51><A HREF="http://csli-www.stanford.edu/hp/TuringTOC.html">Turing's World Table of Contents</A> | <!WA52><A HREF="http://csli-www.stanford.edu/hp/Version-info.html">Information for current users</A> | <!WA53><A HREF="http://csli-www.stanford.edu/hp/Turing5.html">Acknowledgements</A>]

<HR size=4><P>

<!WA54><A HREF="http://csli-www.stanford.edu/hp/Barwise-Etch-100.GIF"><!WA55><IMG SRC="http://csli-www.stanford.edu/hp/Barwise-Etch-25.GIF" border=0></A>  <STRONG>John Etchemendy (left) and Jon Barwise (right) </STRONG><P>

<STRONG><!WA56><A HREF="http://www.phil.indiana.edu/~barwise/barwise.html">Jon Barwise</A></STRONG> is a professor of philosophy, mathematics, and computer science at Indiana University in Bloomington.  His email address is <!WA57><A HREF="mailto:barwise@phil.indiana.edu">barwise@phil.indiana.edu.</A><P>

<STRONG><!WA58><A HREF="http://csli-www.stanford.edu/hp/etchemendy.html">John Etchemendy</A></STRONG> is a professor of philosophy and symbolic systems at Stanford University.  His email address is <!WA59><A HREF="mailto:etch@proof.stanford.edu">etch@proof.stanford.edu.</A><P>

<HR size=4>

<!WA60><A HREF="http://www.stanford.edu/"><!WA61><IMG SRC="http://csli-www.stanford.edu/hp/stanford.seal56.gif" border=0> Stanford Home Page</A> <!WA62><A HREF="http://csli-www.stanford.edu/csli/"><!WA63><IMG SRC="http://csli-www.stanford.edu/hp/logo.csli.gif" border=0> CSLI Home Page;</A>  <!WA64><A HREF="http://csli-www.stanford.edu/publications/">CSLI Publications Home Page</A>  



<HR size=4>


</BODY>
</HTML>
